$\forall$$T$:Type, $c$:$T$, $i$:Id. AtomFree(Type;$T$) $\Rightarrow$ constR\{x:ut2\}($T$; $c$; $i$) $\in$ Realizer